Nuprl Definition : ma-bframe 0,22

M.bframe(k sends on l)
== L != 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M))))))))))(k deq-member(IdLnkDeq;l;L
latex



clarification:

M.bframe(k sends on l)
== fpf-val(KindDeq;
== fpf-val(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M))))))))));
== fpf-val(k;
== fpf-val(k,L.deq-member(IdLnkDeq;l;L)) 
latex


Definitionsz != f(x P(a;z), KindDeq, 1of(t), 2of(t), b, deq-member(eq;x;L), IdLnkDeq
FDL editor aliasesma-bframe

origin